package CTL;
import java.util.Arrays;

import systeme.GrapheRdP;

public class CTLAvant {
	
	GrapheRdP grapheRdp ;

	// Succ
  //  int[][] systeme;
    
    // Donne des valeurs au états
   // boolean[][] AP; 


	public CTLAvant(GrapheRdP graphe){
		
		this.grapheRdp = graphe ;
		
	}
  

    // i -> place 
    // Retourne tableau de boolean taille nombre détat accessible
    // POur indice i regarde si la place est marqué ou non
    public boolean[] prop(int place) {
    	
    	boolean[] res = new boolean[grapheRdp.nbEtat];
    	for (int i = 0 ; i < grapheRdp.nbEtat ; i++){
    		
    		res[i] = grapheRdp.etat.get(i)[place];
    	}
    	
    	return res;
    	
    }

    public boolean[] faux() {
	boolean[] res = new boolean[grapheRdp.succ.size()];
	Arrays.fill(res,false);
	return res;
    }

    public boolean[] vrai() {
	boolean[] res = new boolean[grapheRdp.succ.size()];
	Arrays.fill(res,true);
	return res;
    }

    public boolean[] neg(boolean[] a) {
    int taille = grapheRdp.succ.size() ;
	boolean[] res = new boolean[taille];
	for (int i=0; i<taille; i++)
	    res[i] = !a[i];
	return res;
    }
   
    public boolean[] or(boolean[] a, boolean[] b) {
    	int taille = grapheRdp.succ.size();
	boolean[] res = new boolean[taille];
	for (int i=0; i<taille; i++)
	    res[i] = a[i] || b[i];
	return res;
    }

    public boolean[] and(boolean[] a, boolean[] b) {
    	
    int taille = grapheRdp.succ.size();
	boolean[] res = new boolean[taille];
	for (int i=0; i<taille; i++)
	    res[i] = a[i] && b[i];
	return res;
    }

    public boolean[] EX(boolean[] a) {
    int taille = grapheRdp.succ.size();
	boolean[] res = new boolean[taille];
	for (int i=0; i<taille; i++) {
	    res[i] = false;
	    for (int j=0; !res[i] && j< grapheRdp.succ.get(i).size(); j++)
		res[i] = a[grapheRdp.succ.get(i).get(j)];
	}
	return res;
    }

    public boolean[] AX(boolean[] a) {
	return neg(EX(neg(a)));
    } 

    public boolean[] EU(boolean[] a, boolean[] b) {
	boolean[] res = faux();
	boolean[] avant;
    	do {
	    avant = res;
	    res = or(b,and(a,EX(res)));
	} 
	while(!Arrays.equals(avant,res));
	return res;
    }

    public boolean[] AU(boolean[] a, boolean[] b) {
	boolean[] res = faux();
	boolean[] avant;
    	do {
	    avant = res;
	    res = or(b,and(a,AX(res)));
	} 
	while(!Arrays.equals(avant,res));
	return res;
    }
}